es:ES, R:{R:EE| e, e':E. R(e,e')  (e' < e)} .
(e, e':E. Dec(R(e,e')))
 (p:E(E + Top)
 ((causal-predecessor(es;p)
 (& (e:E.
 (& (((can-apply(p;e))  (e':E. R(e,e')))
 (& (& ((can-apply(p;e))  R(e,do-apply(p;e)))))) 

latex

Definitions

x:A. B(x), Dec(P), x:A. B(x), E, x(s1,s2), ES, P & Q, P  Q, x:A  B(x), b, causal-predecessor(es;p), left + right, Top, {x:A| B(x)} , P  Q, x:AB(x), f(a), , Type, t  T, (e < e'), x. t(x), x.A(x), P  Q, {T}, False, A c B, t.1, A, SqStable(P), T, True, e < e', case b of inl(x) => s(x) | inr(y) => t(y), inl x , inr x , , s = t, Unit, can-apply(f;x), suptype(S; T), do-apply(f;x), S  T, x:A.B(x), Void, P  Q

Lemmas

false wf, true wf, do-apply wf, can-apply wf, assert wf, top wf, iff wf, causal-predecessor wf, it wf, pi1 wf, decidable es-causl, sq stable from decidable, not wf, decidable existse-causl, es-causl wf, decidable wf, es-E wf